pre-init-p(es; i; ds; init; P) == ((P(x.init(x)?)))  (e:E. (loc(e) = i)) 

latex

---

clarification:

pre-init-p(es; i; ds; init; P)
== ((P(x.fpf-cap(init;IdDeq;x;))))  (e:es-E(es). (es-loc(es; e) = i  Id)) 

latex

Definitions

P  Q, b, f(a), x.A(x), f(x)?z, IdDeq, , x:A. B(x), E, s = t, Id, loc(e)